log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
HALF(s(s(x1))) → P(s(s(x1)))
HALF(0(x1)) → 01(s(s(half(x1))))
HALF(0(x1)) → S(half(x1))
HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → S(half(half(x1)))
P(s(s(s(x1)))) → S(p(s(s(x1))))
S(s(p(s(x1)))) → S(s(x1))
LOG(s(x1)) → HALF(s(x1))
P(s(s(s(x1)))) → P(s(s(x1)))
LOG(s(x1)) → LOG(half(s(x1)))
HALF(s(s(x1))) → S(half(p(s(s(x1)))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
LOG(s(x1)) → S(log(half(s(x1))))
HALF(0(x1)) → S(s(half(x1)))
HALF(half(s(s(s(s(x1)))))) → S(s(half(half(x1))))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
HALF(s(s(x1))) → P(s(s(x1)))
HALF(0(x1)) → 01(s(s(half(x1))))
HALF(0(x1)) → S(half(x1))
HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → S(half(half(x1)))
P(s(s(s(x1)))) → S(p(s(s(x1))))
S(s(p(s(x1)))) → S(s(x1))
LOG(s(x1)) → HALF(s(x1))
P(s(s(s(x1)))) → P(s(s(x1)))
LOG(s(x1)) → LOG(half(s(x1)))
HALF(s(s(x1))) → S(half(p(s(s(x1)))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
LOG(s(x1)) → S(log(half(s(x1))))
HALF(0(x1)) → S(s(half(x1)))
HALF(half(s(s(s(s(x1)))))) → S(s(half(half(x1))))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
S(s(p(s(x1)))) → S(s(x1))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(s(p(s(x1)))) → S(s(x1))
The value of delta used in the strict ordering is 1155/16.
POL(s(x1)) = 11/4 + (15/4)x_1
POL(p(x1)) = (7/4)x_1
POL(S(x1)) = (4)x_1
s(s(p(s(x1)))) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
P(s(s(s(x1)))) → P(s(s(x1)))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(s(s(s(x1)))) → P(s(s(x1)))
The value of delta used in the strict ordering is 2.
POL(P(x1)) = (2)x_1
POL(s(x1)) = 1/4 + (2)x_1
POL(p(x1)) = (2)x_1
s(s(p(s(x1)))) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(0(x1)) → HALF(x1)
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(0(x1)) → HALF(x1)
Used ordering: Polynomial interpretation [25,35]:
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
The value of delta used in the strict ordering is 16.
POL(HALF(x1)) = (4)x_1
POL(half(x1)) = (2)x_1
POL(s(x1)) = x_1
POL(p(x1)) = x_1
POL(0(x1)) = 4 + x_1
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(s(0(x1))) → 0(x1)
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
0(x1) → x1
s(s(p(s(x1)))) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(half(s(s(s(s(x1)))))) → HALF(x1)
Used ordering: Polynomial interpretation [25,35]:
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
The value of delta used in the strict ordering is 2.
POL(HALF(x1)) = (4)x_1
POL(half(x1)) = 1/2 + (4)x_1
POL(s(x1)) = x_1
POL(p(x1)) = x_1
POL(0(x1)) = 4 + (2)x_1
half(0(x1)) → 0(s(s(half(x1))))
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(s(0(x1))) → 0(x1)
p(s(s(s(x1)))) → s(p(s(s(x1))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
0(x1) → x1
s(s(p(s(x1)))) → s(s(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
HALF(s(s(x1))) → HALF(p(s(s(x1))))
HALF(half(s(s(s(s(x1)))))) → HALF(half(x1))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LOG(s(x1)) → LOG(half(s(x1)))
log(s(x1)) → s(log(half(s(x1))))
half(0(x1)) → 0(s(s(half(x1))))
half(s(0(x1))) → 0(x1)
half(s(s(x1))) → s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) → s(s(half(half(x1))))
p(s(s(s(x1)))) → s(p(s(s(x1))))
s(s(p(s(x1)))) → s(s(x1))
0(x1) → x1